/bench

Benchmark — ethrex 20 transfers (median of 3)

_{Table parallelism: auto (cores / 3)}

✅ No significant change.

🔬 Looks like a small speedup (-0.3%) — below what 3 runs can confirm. Comment /bench-abba to run the drift-free ABBA tiebreaker (paired-t CI + exact Wilcoxon). Note: it occupies the bench server for ~30–40 min.
Optional pair count: /bench-abba 32 (20 resolves ~1%, 32 for ~0.6%).

✅ Low variance (time: 1.0%, heap: 0.6%)

_{Commit: 1cb8988 · Baseline: cached · Runner: self-hosted bench}

/ai-review

Codex Code Review

Findings

• Low: prover/src/tables/trace_builder.rs still documents the old ECSM / EC_SCALAR / ECDAS flow and says x12/k are read at T with EC_SCALAR byte reads at T+1. The code now reads x12 and k at T+1 and removes EC_SCALAR entirely (line 707, line 718). This timestamp schedule is part of the MEMW proof invariant, so the stale comment can mislead future changes. Update it and the remaining EC_SCALAR doc reference in crypto/ecsm/src/lib.rs.

Open Question

• The PR moves k reads to T+1, but the executor/test rationale still says overlapping xG/k is unprovable because they are read at the same proof timestamp. If overlap rejection is still intended, the rationale should be updated; if not, the guard/test are now stale.

No higher-severity safety, VM semantics, or performance issues found in the PR diff. I did not build or test, per the review constraints.

Review — Feat/ecsm update

Reviewed the EC_SCALAR→ECSM inlining, the xG<p range check, the disjoint memory timestamps, the q1[32] IS_BYTE fix, the ECDAS padding simplification, and the curve-id addition to the ECDAS bus.

The substantive changes look correct and sound:

• ECDAS padding (op=1, q=0, μ-gated R·P): all op-constraints still hold on padding rows (op·next_op=0, next_op·(1-μ)=0, IS_BIT(op)), and the three convolution relations evaluate to 0 at zero carries. Real rows (μ=1) are unchanged; degrees unchanged.
• Bit bus balance: ECSM receives Bit[ts,i] (mult k_bit[i]) for all 256 bits, ECDAS sends per add-round (mult next_op), ECSM sends the MSB. Because ECDAS rounds only reach len_k-1 and the MSB send is at len_k, the balance forces k_bit[len_k]=1 and k_bit[i]=0 for i>len_k — sound.
• xG<p: correct reuse of the byte-path carry-overflow technique; witness (x_g_sub_p), collect_bitwise_from_ecsm, IsHalfword sends, and the +8 constraints are all consistent. Count 411 = 1 + 256 + 8 + 146 checks out.
• Disjoint timestamps: executor (collect_ecsm_ops) and AIR bus sides agree (xG@T, k@T+1 + x12/x10 regs@T+1, xR@T+2); register vs memory use separate is_register namespaces so co-located pointers don't collide. This also resolves the addr_xg == addr_k double-use of (addr, T) the old both-at-T scheme had.
• q1[32] IS_BYTE: consistent across trace / bus / bitwise collection; strictly a completeness fix.
• All ServeK / ec_scalar references are fully removed.

Minor — stale doc comments not updated by this PR:

1. prover/src/tables/trace_builder.rs:654-656 — the collect_ecsm_ops doc still says the x11/x12 register reads and the xG/k memory reads happen at T; the x10 register read and the EC_SCALAR byte reads at T + 1. After this PR the scheme is: x11 + xG at T; x12 + k + x10 at T+1; xR writes at T+2, with no EC_SCALAR byte reads. Since the disjoint-timestamp reorg is the crux of this PR, this comment is now misleading.

2. crypto/ecsm/src/lib.rs:5 — still refers to filling the ECSM / ECDAS / EC_SCALAR trace witnesses; EC_SCALAR no longer exists.

No blocking issues.

AI Review

PR #753 · 12 changed files

Findings

Status column reflects the verdict from the verifier: deepseek-verifier (openrouter/deepseek/deepseek-v4-pro).

Reviewer Lanes

Verification Lanes

Native Codex and Claude reviews run separately and post their own comments. They are not included in this structured provenance report.

Raw lane outputs, candidates, final issues, and model metrics are uploaded as workflow artifacts.

Benchmark Results for unmodified programs 🚀

Responses to AI reviewers

Council of AIs

• AI-001 (IS_BIT on q1[32]): Fixed in 53e31bd — this was a genuine soundness bug
  introduced when removing a reindexing scheme that was later reverted. The IS_BIT
  constraint is back.

• AI-002 (LEN_K unconstrained): False positive. len_k is constrained implicitly by
  the bus balance: the ECSM chip sends exactly 256 BIT interactions for k, so a wrong
  len_k would break bus balance and fail verification.

• AI-003 (256 IS_BIT receivers redundant): False positive. Each of the 256 bit columns
  holds a single bit of k. Without IS_BIT on each one, a malicious prover could set any
  column to an arbitrary field element while still satisfying the bus interaction (which
  only checks the linear combination). The individual IS_BIT constraints are required for
  soundness.

• AI-004 (XgLtP missing from test): Fixed in cd41217 — added OverflowKind::XgLtP
  to the overflow carry constraint loop in constraints_hold_on_generated_trace.

Codex

• Low (stale doc comments in trace_builder.rs and crypto/ecsm/src/lib.rs): Fixed
  in 53e31bd — collect_ecsm_ops doc now accurately describes the disjoint timestamp
  scheme (x11+xG at T; x12+k+x10 at T+1; xR at T+2), and lib.rs no longer references
  EC_SCALAR.

• Open question (executor overlap rationale): Fixed in 53e31bd — the comment now
  explains the actual reason: overlapping addresses would cause the same memory byte to
  serve as both an xG limb and a k bit, corrupting the scalar multiplication. The overlap
  guard is still intentional and correct.

Claude

• Minor (stale doc comments): Fixed in 53e31bd — same as Codex finding above.